Inference at * 1 1 1 2 2 
Iof proof for Lemma decidable implies better:



1. P : 
2. Q : x:P.
3. P
4. Q
5. Q  
  (P  Q)  ((P  Q)) 

latex

 by OrRight THEN Auto  
THEN D 0 THEN Auto  

latex

TH1: 

TH1: 6. P  Q
TH1:   False
TH.

Definitions

P  Q, {T}, A, False, P  Q, , t  T